The invention relates to a method of automated proving for unrestricted first-order logic to test the satisfiability of clause sets describing an industrial system, the resulting automated proving tool and industrial system, and the information carrier incorporating a program carrying out the method.
Automated proving is concerned with the fundamental task of establishing the satisfiability or unsatisfiability of formula sets including cl use sets. A computational method dedicated to this task is called a proof method. Automated proving is involved in various logical computations which will be here covered by the global notion of automated reasoning: e.g. computation of counter-models of formula sets, automated theorem proving, computation of maximal satisfiable subsets of unsatisfiable sets of formulas, computation of minimal support of theorems, etc. The invention can be used by any industrial application where first-order logic automated reasoning can be explicitely or implicitely involved.
First-order logic has become of industrial interest through a restricted sublogic known as Horn clause logic. Horn clause formalism is used by logic programming languages like PROLOG both as a declarative and imperative language. The wide variety of applications which can be achieved with logic programs illustrates the versatility of Horn clause logic in expressing various problems (for example, see: xe2x80x9cArtificial Intelligence through PROLOGxe2x80x9d, Prentice Hall 1988, Rowe, N. C.). But in many cases the expressive power of Horn clause logic is not sufficient: unrestricted first order logic, and even higher-order logic, is needed. How to use unrestricted first-order logic in expressing problems or in describing digital circuits, computer programs, complex systems, etc, and how first-order logic automated reasoning allows computers to solve such problems is explained in many classical textbooks (for example, see: xe2x80x9cAutomated Reasoningxe2x80x9d, Prentice Hall,1984, Wos, L. et al.).
Thus, beyond those related to Horn clause logic programming, there is a wide range of industrial applications where, explicitely or implicitely, first-order logic automated reasoning can be involved and the invention used, among which can be mentioned, for example:
General purpose automated reasoning systems: general purpose automated reasoning systems can be sold or distributed as stand-alone products (software products or dedicated machines) and/or within packages. They can be used to train or help mathematicians, logicians, computer scientists and any kind of end-users in checking and/or proving the validity and/or the satisfiability and/or the unsatisfiability of all kinds of statements which can be expressed in the forms accepted by the end-user interfaces and which can be translated in logic, this including among others various logical formalisms, pseudo-natural languages, graphic inputs, and any kind of dialog based interactions with users. General purpose automated reasoning systems may also provide more sophisticated functionalities, based on the computation of maximal satisfiable subsets of unsatisfiable sets of statements and/or the computation of minimal unsatisfiable subsets of given sets of statements. General purpose automated reasoning systems may also be used by other devices (softwares or hardwares) through various specific communication channels.
Truth maintenance systems: truth maintenance systems can be sold and/or distributed as stand-alone products or within artificial intelligence packages. They are oriented toward automatic verification of the satisfiability of sets of statements expressing various kinds of knowledge or specifications. They may also provide help for management of unsatisfiable sets of statements through computation of maximal satisfiable subsets. They may also provide tools to analyze logical dependencies between formulas and help minimize logical knowledge bases through computation of minimal unsatisfiable subsets.
Building and/or exploitation environments for knowledge based systems: they may incorporate more or less implicitly truth maintenance functionalities, and may also use automated proving to answer queries and draw conclusions from knowledge bases in exploitation mode.
Database management and exploitation systems: as environments for knowledge based systems, they may incorporate more or less implicitly truth maintenance functionalities in order to verify database conceptual schemas, and may also, in exploitation mode, use automated proving to answer queries about deductive databases.
Domain-oriented specific applications using implicitly or explicitly first-order logic automated reasoning, like, for example, fault-finding, diagnosis, maintenance, reliability analysis, prevision systems, etc, in various domains like, for example, technical, medical, financial, etc.
Methodological tools for the conception of information systems: conceptual schemas of information systems for enterprises and administrations of various scales can be translated into logic, and then formally checked with automated reasoning.
Software libraries (sources and/or object codes) or hardware co-processors which can be sold or distributed as stand-alone products or in packages, providing routines related to automated reasoning.
Formal verification and symbolic simulation of the specifications of dynamical devices or systems. When parts or totality of the specifications, at some level of discrete abstraction for continuous physical systems, can be expressed or translated in logic, various verifications of properties fulfillment can be performed by automated reasoning. In case of violation of some required properties, truth maintenance functionalities may be used to restore correctness. Automated reasoning may also be used to simulate in more or less instantiated context the behavior of the specified device or system. In this class of applications there are, for example:
formal verification and symbolic simulation of the specifications of various finite state machines: for example digital circuits, man/machine interfaces, etc.
formal verification and symbolic simulation of program specifications.
formal verification and symbolic simulation of the specifications of concurrent systems.
formal verification and symbolic simulation of the specifications of communication protocols.
formal verification and symbolic simulation of the specifications of complex systems, e.g. nuclear reactors, emergency plans, etc.
etc.
Formal verification, formal comparison to specifications and symbolic simulation of the description of real devices or systems. As with formal verification of specifications, except that there it is some logical description of real devices or systems which is of concern. Moreover, if specifications are available, the conformity of a real: system to its specifications can be checked by automated reasoning. In this class of applications there are, for example:
formal verification and symbolic simulation of various finite state machines: for example digital circuits, man/machine interfaces, etc.
formal verification and symbolic simulation of programs.
formal verification and symbolic simulation of concurrent systems.
formal verification and symbolic simulation of communication protocols.
formal verification and symbolic simulation of complex systems, e.g. nuclear reactors, emergency plans, etc.
etc.
Security analysis of programs, information and decision flowcharts.
Currently available proof methods for first-order logic have a common drawback. They cannot provide simultaneously a level of performance and a degree of robustness sufficient to fulfill industrial needs.
Currently available proof methods rely on some common basic principles which give them a great propensity to waste time in performing redundant operations, except when by chance they quickly find a proof. As a consequence they have a great lack of robustness: robustness means here completeness and soundness plus regularity of performance on problems of similar complexity and also boundedness for most solvable problems. In order to be more robust, these proof methods have to be augmented with curative strategies which do not prevent them from performing redundant operations but just delete some of the unneeded results that they record. These curative strategies are rather time an space consuming while, however, they do not always bring enough robustness. On the other hand, among the available proof methods the only one which may reach a significant level of performances for industrial purpose are those inspired by the interpretation and compilation methods currently used for Horn clause logic programming languages like PROLOG, methods which can be extended to cope with unrestricted first-order logic (see for example: xe2x80x9cComputing with Logicxe2x80x9d, Benjamin/Cummings 1988, Maier, D. and Warren, S.). Good performance is obtained at the price of a complete lack of robustness, which makes this kind of approach rather useless except in the particular context of programming languages intended to be used by careful and skilled programmers.
A detailed analysis of this common drawback is now discussed. Note that the notions which are of current use in automated proving literature are all precisely defined in the bibliographical references mentioned below. Most of these notions (e.g. clause, literal, most general unifier, substitution, etc) will be used here without any recall of their definition. However, it may be referred to the preliminary recalls presented as an introduction of the description of the present method. The first mention of any notion which is new or not of current use in automated proving literature will be marked by the use of italic letters. Italic letters will be also used when introducing a notion with a definition differing from the definition which can be found in the bibliographical references.
Available proof methods for full first-order logic are refutation deduction systems of which aim is to deduce a contradiction, i.e. a formula which is obviously unsatisfiable, from unsatisfiable formula sets. A refutation deduction system can be algorithmically defined as being a loop of which exit condition is the presence in the current formula set of a contradiction or the impossibility to apply its deduction rules to the current formula set in order to perform a new deduction step. At each iteration of this loop is chosen a particular deduction step among all those which can be performed. This selected deduction step is then executed, the resulting formula being added to the current formula set. Note that theorem proving can be achieved by refutation deduction systems thanks to the following property: a formula is a theorem for a set of proper axioms if and only if this set of axioms when augmented with the negation of the formula becomes unsatisfiable.
Most of these proof methods use deduction rules which are refinements or slight modifications of Robinsons resolution principle on formulas in clausal form. Theoretical and practical issues of such resolution-based proof methods are comprehensively documented in many classical textbooks (for example, see: Symbolic Logic and Mechanical Theorem Proving Academic Press 1973, Chang, C. L. and Lee, R. C. T., or An Introduction on Automated Deduction by Stickel, M., E. in Fundamentals of Artificial Intelligence p. 75-35 133, Springer-Verlag 1986).
The source of the propensity of currently available proof methods to perform redundant operations relies in their deductive nature. A deduced formula is, by definition, always logically redundant with the initial formula set from which it is deduced: it just duplicates and combines pieces of logical information already expressed separately in the initial formula set. A contradiction is produced when two directly uncompatible pieces of information are combined together. Thus, refutation deduction systems while duplicating pieces of informations have generally growing chances to perform recombinations of already combined pieces of information.
A refutation proof is a sequence of deduction steps leading from the initial formula set to a contradiction and where all deduction steps are needed to deduce this contradiction. A deduction step will be said intrinsically useless for proof purpose when it cannot occur in any refutation proof. A deduction step will be said redundant for refutation purpose when, if occurring in some proofs, already performed deduction steps could replace it to build similar proofs. In other words a deduction step is redundant when it does not produce a formula closer to a contradiction than already available ones.
A refutation method is said complete when for any unsatisfiable formula set it is guaranteed to always find a refutation proof after a finite number of steps. A proof method is said bounded on a class of solvable problems when it is guaranteed to reach a decision after a finite number of deduction steps for any problem of this class: when a proof method is bounded on a class of problems it is a decision procedure on this class. For most satisfiable formula sets, the number of possible deduction steps is a priori not finite. Thus boundedness on such problems relies exclusively on skill in discarding intrinsically useless and redundant deduction steps. For a given proof method the apparent complexity of a problem is related to the number of deduction steps that it would pave to perform with a breadth-first search strategy before to reach a conclusion. But the real complexity of a problem is rather related to the number of deduction steps that would have to be performed to reach a conclusion if all intrinsically useless or redundant deduction step were preventively discarded. So two problems of similar real complexity may appear to be of quite different complexity to methods which do not discard enough redundant and useless deduction steps. Thus regularity of performances relies, like boundedness, essentially on skill in avoiding useless or redundant deduction steps.
Resolution-based methods can use two kinds of deletion strategies to become more robust: preventive deletion strategies and curative ones. Tautologies and clauses with a pure literal can be deleted from the current clause set because any resolution step involving such clauses would be intrinsically useless. The deletion strategy eliminating clauses with a pure literal is called purity. Tautology elimination and purity elimination are preventive strategies avoiding the execution of intrinsically useless deduction steps. Deletion of subsumed clauses is a strategy called subsumption. Subsumption is a curative strategy. It provides a means to discard the effects of the most obviously redundant deduction steps after they have been performed: it does not prevent their execution.
Subsumption requires, each time a new clause is produced, to compare it with the ones already present in the clause set. This is time consuming. However, even with subsumption, resolution remains unbounded for simple problems of the Bernays-Schxc3x6nfinkel class, i.e. the class of problems expressed by clauses without functional terms. This is quite surprising as problems of this class have always a finite Herbrand Universe. This illustrates well that subsumption does not detect all the undesirable effects of redundant deduction steps and thus cannot bring, despite its computational cost, enough robustness to resolution.
Basic resolution, also called binary resolution, can be refined in order to consider more than one link at one and the same time. This refinement is called hyperresolution. Each hyperresolution step does the deductive job of several binary resolution steps, and there are less possible deduction steps than with binary resolution. However, if hyperresolution leads to perform less deduction steps than binary resolution, it shows still a great propensity to perform redundant deduction steps.
Resolution, hyperresolution and subsumption have all been invented in the same year, 1965, by J. Robinson. Since this time, most of research works in the field of automated proving have been devoted to ameliorate the performances of binary resolution and hyperresolution deduction systems, mainly through the addition of various restriction strategies: i.e. strategies which, at each iteration of the loop, forbid to consider as possible candidates for execution the deduction steps which are not in some restricted subset of the complete set of all the possible ones. Like the replacement of binary resolution by hyperresolution, these restriction strategies may provide better performances but none of them can both preserve completeness and correct sufficiently the propensity of deduction systems to perform redundant operations.
To find satisfying solutions to this common drawback of resolution deduction systems, from the above constatations, it seems required to move away from Robinson""s principles. Since 1965 until now there have been only three proposals which go in this direction. The first one, Kowalski""s link removal in clause graph resolution, starts with classical Robinsons resolution but adds a means to discard certain links before they can be used: the resulting system is no longer a classical resolution deduction system, and this brings often a very significant enhancement over Robinson""s deductive approach while this also may lead sometimes to unacceptable flaws of behavior. The two other proposals, are relying on classical deduction systems but replace resolution by other deduction rules.
Now Kowalski""s link removal will be considered. Resolution applies on links between complementary literals occurring in different clauses of the clause set. A preventive strategy would eliminate redundant links before they are resolved. This would require to understand why a link may be a priori redundant, which is a question never considered by curative strategies like subsumption. Another benefit would be that eliminating redundant links before they are resolved leads to much more pure literals in consequence purity may then eliminate much more clauses.
This idea is the basis of clause graph resolution, in short cg-resolution, introduced by R. Kowalski in 1975 (for example, see: xe2x80x9cProperties of Clause Graph Resolutionxe2x80x9d, Morgan Kaufman Publishers 1991, Eisinger N.). Instead of clause sets it operates on clause graphs, where vertices are individual clauses and the edges are links between clauses. Clause graph resolution links contribute to the logical meaning as well as clauses. This allows to remove some redundancy of logical information by removing links instead of clauses. On the other hand it is needed to compute and store all the possible links between clauses, which may be time and space consuming. Links of derived clauses are not directly computed but rather inherited from their parent clauses. When two clauses are resolved upon a link, this link is removed from the set of available links. Then, this removed link cannot be inherited by new clauses which could be derived afterwards. This particular deletion strategy of cg-resolution is called link removal: it does not eliminate clauses but discard links. Note that without link removal, cg-resolution would behave exactly like standard resolution. Thanks to link removal, derived clauses may have much less links with other clauses in cg-resolution than in standard resolution and thus much less deduction steps are allowed. This, in combination with purity, often leads to very significant pruning of the search space and proportional gains in performances over standard resolution.
However, cg-resolution can run forever without reaching any decision on some satisfiable sets of ground clauses: cg-resolution is unbounded on the ground level which is not the case of standard resolution augmented with subsumption. The reason for this first flaw is that link removal does not preventively discard enough of the redundant links that standard resolution would have considered, while it makes things much too complicated to use subsumption in complement, as freely as needed. A second flaw of cg-resolution is that link removal may also prevent the consideration of some links which are not redundant: in such a case cg-resolution may run forever or conclude erroneously that the initial clause set is satisfiable while it is in fact unsatisfiable. This last flaw is related to the fact that cg-resolution is not a classical deduction system: link removal may have as effect that after a resolution step the resulting clause graph: is not logically equivalent to its previous state, and thus clauses which were deductible from this previous state may become non deductible after a resolution step. The flaw occurs when among the clauses which become non deductible is the empty clause that resolution is intended to produce.
These two flaws show that link removal is lacking a sound theoretical foundation. Link removal is not relying on a deep understanding of the reasons why a link could be redundant: it is rather a tricky strategy which gives often very good results while, sometimes, unacceptable behaviors may result from it. However, since 1975 until now, no other idea has been published to prevent redundant deduction steps by discarding preventively redundant links. It may be suspected from this constatation that a strong and safe preventive avoidance of redundant deduction steps may well be impossible in the context of resolution-based proof methods.
We now examine non resolution-based proposals which move away from Robinson""s principles by replacing resolution or hyperresolution by alternative deduction rules.
A first direction to move away from resolution and hyperresolution deduction rules is illustrated by Bibel""s connection method (see: xe2x80x9cAutomated theorem provingxe2x80x9d, Vieweg 1987, Bibel W.).
A path of a clause set is any list of literals such that each element of this list occurs in a different clause. A path is said complete when its length is the cardinal of the clause set. A connection is any pair of opposite literals. The leading principle of Bibel""s connection method is the following for the propositional ground level. To refute a clause set it is sufficient to compute the set of its complete paths which do not include a connection: if this set is empty the initial clause set is refuted otherwise it is proved satisfiable. This method can be viewed as a deduction system relying on the following deduction rule that we shall name superclausal conjunction: from two formulas in disjunctive normal form derive their logical conjunction expressed also in disjunctive normal form. It is assumed there that the rewriting under disjunctive normal form always removes all the conjunctions of literals when two opposite literals occur: this comes just to discard paths including a connection. Below we shall call superclause any quantifier-free formula in disjunctive normal form. As a clauses is a disjunction of literals, a superclause is a disjunction of what we call superliterals, a superliteral being itself a conjunction of literals. The notion of superclause generalizes the usual notion of clause as clauses are just superclauses with every superliteral being a single literal. Then the superliterals of a superclause resulting of the logical conjunction of several different clauses are just the conjunctive expression of the connection-free complete paths of the set of these clauses. Clauses are often presented as lists or sets of literals, their disjunctive nature being left implicit. Superclauses can in the same way be represented as (disjunctive) sets of (conjunctive) sets of literals. In this case superliterals are sets resulting of a simplification of paths (elimination of duplicate literals and reduction to the empty set when a connection is included). To get a complete refutation system it is sufficient to apply the superclausal conjunction rules on superclauses which have a connection, i.e. one of the superliterals of their superclausal conjunction will be reduced to the empty superliteral because of the occurrence of two opposite literals.
The parent superclauses involved in a superclausal conjunction step can be safely removed as soon as the superclause resulting of their conjunction is generated. Thus superclausal conjunction is not a simple deduction rule but rather a transformation rule on superclause sets which safely removes parent superclauses when it adds their derived child. Using such a kind of transformation rule has the nice property of avoiding the duplication of pieces of logical information inherent to the use of deduction rules.
However when climbing from the propositional ground level to the first-order level things become much more complicated and the good property obtained on the ground level is lost. At the first-order level there are not only connections but also links within complementary literals which can become opposite only after the application of a non empty most general unifier. In this case, the superclausal conjunction will compute the conjunction of strict instances of the parent clauses and then the parent clause cannot be removed without loosing completeness. Moreover a second deduction rule must be used in order to generate instances of superclauses resulting from the reduction of links internal to superliterals. Thus, at the first-order level, the connection method is faced with the same drawback as resolution, that it may even considerably amplify. As a consequence, the connection method to be both complete and of practical use, has to be refined: instead of dealing with superclauses through superclausal conjunction, it rather uses rules dedicated to the expansion and reduction of individual paths. But it then appears that with these kind of refinements the connection method becomes quite similar to a slight modification of resolution, known as model elimination procedure.
Thus Bibel""s connection method as other methods which follow the same lines of inspiration, while quite different from resolution in their conceptual principle, do not open in practice really new ways to build efficient and robust proof methods.
Now we examine a second alternative to resolution, which can be illustrated by a method recently proposed in 1992 by Lee and Plaisted.
A superficial examination of resolution would conclude that it is a very simple deduction rule and that it would be useless to seek alternative rules to base on proof methods. The disappointing collapse of the connection method, when refined to be of practical use, to a well-known kind of resolution seems also in favor of such a conclusion. But a deeper examination shows that resolution is indeed much more complicated than it seems to be. It can be analyzed as the intricate mix of two more basic operations: ground resolution and another operation that we shall call here link: instance generation. Link instance generation is a deduction rule which derives instances of a pair of clauses by applying to them a most general unifier related to one of their common links. Ground resolution is a deduction rule which operates on the propositional ground level. A refutation deduction system using only ground resolution is sound and complete for propositional logic. Moreover, augmented with subsumption, ground resolution is bounded on propositional logic and thus the combination of ground resolution with subsumption provides a decision procedure for propositional logic. In order to cope with logical variables of the first-order level, ground resolution is mixed with link instance generation which is only concerned with first-order specific features. The result is the standard resolution rule for first-order logic, which can be further refined to become hyperresolution. Then, as it has already been mentioned, the combination of resolution with subsumption is unbounded for some almost propositional problems which would have to be very easy to solve by any useful proof method. A conclusion which may be drawn from this is that mixing in an unique operation two more basic operations of different concerns, like ground resolution and link instance generation are, may well be an important source of difficulties that would not appear if these operations were kept separate.
This is the idea underlying a new proof method proposed by Lee and Plaisted in 1992 (in xe2x80x9cEliminating Duplication with the Hyper-Linking Strategyxe2x80x9d, Journal of Automated Reasoning 1992, Vol. 9, pages 25-43, Lee, S. J. and Plaisted, D. A.). In this method, contrarily to resolution, the obtention of a refutation is not due to an unique rule. There are in fact two independent submethods which are interacting: a deductive system using two kinds of instance generation rules, and a proof method dedicated to the propositional ground level. This last submethod dedicated to the propositional ground level is not based on ground resolution but on a more efficient approach inspired by Davis and Putnam algorithm (see, for example, Journal of the ACM, Vol. 7, 1960, pages 201-205 xe2x80x9cA computing Procedure for Quantification Theoryxe2x80x9d Davis, M. and Putnam, H.). The deduction system uses a rule that Lee and Plaisted call hyper-link operation and which is a refinement of link instance generation similar to what hyperresolution is to binary resolution (in the related publication, Lee and Plaisted call link operation what we call here link instance generation, and hyper-link operation what we shall call hyper-link instance generation). There is also a second instance generation rule which derives from each non ground clause a ground instance obtained by replacing any variable by a same constant. We shall call this particular instance generation rule a ground instance generation. In their publication Lee and Plaisted prove that a deduction system using only link or hyper-link instance generation and ground instance generation, when augmented by any sound and complete proof method for propositional logic, is then sound and complete for first-order logic: Moreover they show that, on a class of problems that they call near-propositional problems, their method can provide much better performances than resolution or hyperresolution.
In this approach proposed by Lee and Plaisted, the deduction system which iteratively applies instance generation rules, as it is a deduction system, shows a great propensity to perform redundant deduction steps. While it is not mentioned in the related publication, the deletion strategies already employed by resolution-based methods can be adapted to instance generation systems, e.g., purity, subsumption or link removal. But there subsumption cannot be entirely applied as with instance generation any derived clause is subsumed by its parent clause. It is only a simplified kind of subsumption which can be used: elimination of variant clauses.
A clause generated by instance generation is subsumed by its parent clause from which it is drawn. Contrary to what happens in resolution, subsumed clauses cannot be removed as this would lead to discard any generated clause: two variant clauses are completely redundant for refutation purpose because their respective child clauses generated by ground instance generation would be identical.
Note that an instance generation system when augmented with elimination of variant clauses is obviously bounded on the Bernays-Schxc3x6nfinkel class of problems. However, Lee and Plaisted remark that detecting and eliminating duplicate clauses, which is a simplified kind of variant elimination, is yet quite time consuming for their method and they cite as a possible alternative link removal on clause graphs. Link removal can be adapted to link instance generation on clause graphs: each time a link instance generation is performed upon a link, the link can be removed from the parent clauses. But, as already seen, with link removal the boundedness property which is obtained for some interesting class of solvable problems may well be easily lost. This was the first flaw of link removal in cg-resolution which remains true for instance generation systems: link removal does not discard enough redundant links while it makes things too complicated to apply freely a complementary curative strategy like elimination of variant clauses. However, the second flaw of link removal in cg-resolution, the possibility that some clause may become non deductible while it was previously deductible from the initial clause graph, cannot happen when link removal is applied to instance generation systems: for such systems link removal just prevents redundant deduction steps to be performed and it does not delete any non redundant information.
As it is proposed, the method of Lee and Plaisted seems of little interest for problems which are far from being of the near-propositional kind. With resolution, the literals of the parent clauses which are involved in a link are discarded from the resolvent clause while these literals are still present in the derived clauses with link instance generation rule. And in cases where functional terms play an important role and where possible proofs may be of a non neglectable minimal length, this may lead to perform much more redundant deduction steps than with resolution.
In conclusion, as Lee and Plaisted do not propose or even suggest in their publication any new strategy to prevent redundant instance generations. Their particular proof method is not of a greater practical interest, and in fact it is of a much lower pratical interest, than resolution-based ones, except when dealing with near-propositional problems.
Proof methods which, like Lee and Plaisted""s method, keep separate instance generation rules and propositional ground level operations will be called instance generation methods.
More generally, the background of the present invention can also be found in the following documents:
Andrews, P. B., Refutations by matings, IEEE Transactions on Computers, Vol. C-25 (1976), pages 801-806;
Andrews, P. B., Theorem Proving via General Matings, Journal of the ACM,.Vol. 28 (1981), pages 193-214;
Billon, J. P., Perfect Normal Forms for Discrete Functions, Bull research report (June 1987);
Billon, J. P. and Madre J. C., Original concepts of PRIAM, an Industrial Tool for Efficient Formal Verification of Combinatorial Circuits, in The Fusion of Hardware Design and Verification, G. J. Milne editor, North-Holland publishers (1988);
Bryant, R. E., Graph-based Algorithms for Boolean Functions Manipulations, IEEE transactions on Computers, Vol. C35 (1986), pages 677-691;
Bryant, R. E., Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams, ACM Computing Surveys, Vol. 24 (1992), pages 293-318;
Eisinger, N., Completeness, Confluence and Related Properties of Clause Graph Resolution, Pitman (1991);
Joyner, W. H., Resolution Strategies as Decision Procedures, Journal of the ACM, 23 (1976), pages 398-417;
Kowalski, R. and Kuehner, D., Linear Resolution with Selection Function, Artificial Intelligence, Vol. 2 (1971), pages 227-260;
Kowalski, R., A Proof Procedure Using Connection Graphs, Journal of the ACM, Vol. 22 (1975), pages 572-595;
Kowalski, R., Logic for Problem Solving, Elsevier (1979);
Loveland, D. W., A Simplified Format for the Model Elimination Procedure, Journal of the ACM, Vol. 16 (1969), pages349-363;
Loveland, D. W., Automated Theorem Proving a Logical Basis, North Holland (1978);
Letz, R., Schumann, J., Bayerl, S. and Bibel, W., SETHEO xe2x80x9cA High-Performance Theorem Proverxe2x80x9d, Journal of Automated Reasoning, Vol. 8 (1992), pages 183-212;
Madre, J. C, Coudert, O., Billan, J. P. and Berthet, C., Formal Verification of Digital Circuits Using a Propositional Theorem Prover, Proceedings of the IFIP Working Conference on the CAD Systems Using AI Technics, Tokyo (1989);
Robinson, J. A., a Machine-oriented Logic based on the Resolution Principle, Journal of the ACM, Vol. 12 (1965), pages 23-41;
Robinson, J. A., Logic Form and Function, Edinburgh University Press (1979):;
Shostak, R., Refutation Graphs, Artificial Intelligence, Vol. 7 (1976), pages 51-64;
Smullyan, R. M., First-order Logic, Springer, Berlin (1968).
The invention relates to a new proof method for unrestricted first-order logic, providing simultaneously a level of performance and a degree of robustness that could not be provided by any currently available proof method and can be sufficient to fulfill industrial needs.
The invention relates to a method of automated proving for unrestricted first-logic to test the satisfiability of clause sets describing an industrial system, comprising applying the instance generation rule       (    IG    )    ⁢      xe2x80x83    ⁢      Ψ          Ψ      ⁢              xe2x80x83            ⁢      σ      
where xcexa8 is a term, "sgr" a substitution and xcexa8"sgr" an instance of xcexa8 yielded by the substitution "sgr", characterized in that, defining an instance subtraction as the subtraction of the instance xcexa8"sgr" from xcexa8 resulting in a generalized term which is a triplet  less than xcexa8, "sgr", xcex9 greater than  where xcex9 is a finite set of standard substitutions {xcex1, . . . , xcexn} and defined by
GE( less than xcexa8, "sgr", xcex9 greater than )=GE(xcexa8"sgr")xe2x88x92GE({xcexa8xcex1, . . . , xcexa8xcexn})
the method further applies an instance subtraction combined with said instance generation rule to get an instance extraction rule defined by
(IE)xcexa3xe2x86x92(xcexa3xe2x88x92{xcexa8 less than "sgr", xcex9 greater than })∪{xcexa8 less than "sgr"xcexc, xcex9*"sgr"xcexc greater than , xcexa8 less than "sgr", xcex9∪{"sgr"xcexc} greater than )
where xcexa3 is a set of clauses and xcexc is a substitution valid for the generalized term xcexa8 less than "sgr", xcex9 greater than , whereby the set xcexa3 can be proved unsatisfiable.
Optionally, when defining a half-unifier of the term xcexa8 for a term "PHgr" as a substitution "sgr" such that the instance xcexa8"sgr" is an instance of "PHgr", and a most general half-unifier as a half-unifier yielding a most general instance, the instance extraction comprises a link instance generation modified to become a half-link generation rule defined by       (    HIG    )    ⁢      xe2x80x83    ⁢            Ψ      ,      Φ                      Ψ        ⁢                  xe2x80x83                ⁢        σ        ⁢                  xe2x80x83                ⁢        1            ,              Φ        ⁢                  xe2x80x83                ⁢        σ        ⁢                  xe2x80x83                ⁢        2            
where "sgr"1 and "sgr"2 are two complementary most general half-unifiers of the literals of a link between xcexa8 and "PHgr".
A list or a set of superliterals which are themselves a list or a set of literals being called a superclause, the method further comprises translating clauses into superclausal formalism and applying an instance generation on superclause sets.
Thus, an Extract-Minimal-Half function can be computed from an algorithm defined as
Extract-Minimal-Half(mgu, tag):
Let Res be a copy of mgu where all variables tagged by tag are replaced by untagged variables of same name
Remove from Res all unit substitutions on tagged variables;
% minimization loop %
Forall unit substitution u in Res do:
When the right side of u is a tagged variable replace in Res all occurrences of this variable by the left side of u and remove u from Res;
Replace remaining tagged variables in Res by new untagged variables;
Return Res;
Additionally, in defining a near-quasi-connection when its related most general unifiers and most general half-unifiers contain only unit substitutions which associate variables to variables, the method can use the property that the ground set corresponding via ground instance generation to a clause or superclause set has a complete spanning set of connections if and only if this last set has a complete spanning of near-quasi-connections, so that a ground instance generation can be avoided.
The method can also apply a purity elimination strategy, the purity being defined in superclausal formalism when a superliteral is pure, i.e., if it has neither external link nor internal link and/or a tautology elimination strategy and/or a unit-reduction.
Furthermore, the method can use hyper-half-links, a hyper-half-link of a clause being a list of half-links of the clause or superclause such that there is in this list one and only one half-link of each of the literals of the clause or each of the superliterals of the superclause, so that a hyper-half-link generation complies with the rule       (    HHIG    )    ⁢      xe2x80x83    ⁢      Ψ          Ψ      ⁢              xe2x80x83            ⁢      θ      
where xcex8 is the substitution associated to a valid hyper-half-link of xcexa8.
In this case, a generalized superclause being said hyperpure when it has; no valid hyper-half-link, the hyper-half-link generation can further comprise a superpurity elimination strategy of eliminating hyperpure superclauses instead of a purity elimination strategy.
It will be shown that the invention relates to four innovative enhancements which can be done to a family of proof methods for first-order logic that we call instance generation methods. Each of the four enhancements preserves the completeness and the combination with one another also preserves the completeness.
The invention further relates to the automated proving tool carrying out the method of the invention and the industrial system resulting from the application of this method it also relates to an information carrier, such as a magnetic tape or disk, incorporating a program carrying out the method of the invention.